(s1  s2 mod x) == z:Id. z = x  s1(z) = s2(z) 

latex

---

clarification:

ma-x-equiv(M;x;s1;s2) == z:Id. z = x  Id  s1(z) = s2(z)  M.ds(z) 

latex

Definitions	x:A. B(x), P  Q, A, Id, s = t, M.ds(x), f(a)
FDL editor aliases	ma-x-equiv